\begin{tabbing}
$\forall$$f$:($\mathbb{N}\rightarrow\mathbb{Q}$).
\\[0ex]($\forall$$n$:$\mathbb{N}$. 0 $\leq$ $f$($n$))
\\[0ex]$\Rightarrow$ \=($\forall$$k$:$\mathbb{N}$, $g$:(\{0..($k$+1)$^{-}$\}$\rightarrow\mathbb{N}$).\+
\\[0ex]($\forall$$n$:\{0..($k$+1)$^{-}$\}, $i$:\{0..$n$$^{-}$\}. ($g$($i$)) $<$ ($g$($n$)))
\\[0ex]$\Rightarrow$ \=$\Sigma$0 $\leq$ $i$ $<$ $k$\+
\\[0ex]$f$($g$($i$)) $\leq$ $\Sigma$0 $\leq$ $i$ $<$ $g$($k$)
\\[0ex]$f$($i$))
\-\-
\end{tabbing}